0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 86 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 197 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 PiDPToQDPProof (⇒, 10 ms)
↳23 QDP
↳24 QDPSizeChangeProof (⇔, 0 ms)
↳25 YES
INORDERD_IN_GA(tree(nil, X1, X2), X3) → U8_GA(X1, X2, X3, inorderA_in_ga(X2, X4))
INORDERD_IN_GA(tree(nil, X1, X2), X3) → INORDERA_IN_GA(X2, X4)
INORDERA_IN_GA(tree(X1, X2, X3), X4) → U1_GA(X1, X2, X3, X4, inorderA_in_ga(X1, X5))
INORDERA_IN_GA(tree(X1, X2, X3), X4) → INORDERA_IN_GA(X1, X5)
INORDERA_IN_GA(tree(X1, X2, X3), X4) → U2_GA(X1, X2, X3, X4, inordercA_in_ga(X1, X5))
U2_GA(X1, X2, X3, X4, inordercA_out_ga(X1, X5)) → U3_GA(X1, X2, X3, X4, inorderA_in_ga(X3, X6))
U2_GA(X1, X2, X3, X4, inordercA_out_ga(X1, X5)) → INORDERA_IN_GA(X3, X6)
U2_GA(X1, X2, X3, X4, inordercA_out_ga(X1, X5)) → U4_GA(X1, X2, X3, X4, X5, inordercA_in_ga(X3, X6))
U4_GA(X1, X2, X3, X4, X5, inordercA_out_ga(X3, X6)) → U5_GA(X1, X2, X3, X4, appendB_in_ggga(X5, X2, X6, X4))
U4_GA(X1, X2, X3, X4, X5, inordercA_out_ga(X3, X6)) → APPENDB_IN_GGGA(X5, X2, X6, X4)
APPENDB_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → U6_GGGA(X1, X2, X3, X4, X5, appendB_in_ggga(X2, X3, X4, X5))
APPENDB_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPENDB_IN_GGGA(X2, X3, X4, X5)
INORDERD_IN_GA(tree(tree(X1, X2, X3), X4, X5), X6) → U9_GA(X1, X2, X3, X4, X5, X6, inorderA_in_ga(X1, X7))
INORDERD_IN_GA(tree(tree(X1, X2, X3), X4, X5), X6) → INORDERA_IN_GA(X1, X7)
INORDERD_IN_GA(tree(tree(X1, X2, X3), X4, X5), X6) → U10_GA(X1, X2, X3, X4, X5, X6, inordercA_in_ga(X1, X7))
U10_GA(X1, X2, X3, X4, X5, X6, inordercA_out_ga(X1, X7)) → U11_GA(X1, X2, X3, X4, X5, X6, inorderA_in_ga(X3, X8))
U10_GA(X1, X2, X3, X4, X5, X6, inordercA_out_ga(X1, X7)) → INORDERA_IN_GA(X3, X8)
U10_GA(X1, X2, X3, X4, X5, X6, inordercA_out_ga(X1, X7)) → U12_GA(X1, X2, X3, X4, X5, X6, X7, inordercA_in_ga(X3, X8))
U12_GA(X1, X2, X3, X4, X5, X6, X7, inordercA_out_ga(X3, X8)) → U13_GA(X1, X2, X3, X4, X5, X6, appendB_in_ggga(X7, X2, X8, X9))
U12_GA(X1, X2, X3, X4, X5, X6, X7, inordercA_out_ga(X3, X8)) → APPENDB_IN_GGGA(X7, X2, X8, X9)
U12_GA(X1, X2, X3, X4, X5, X6, X7, inordercA_out_ga(X3, X8)) → U14_GA(X1, X2, X3, X4, X5, X6, appendcB_in_ggga(X7, X2, X8, X9))
U14_GA(X1, X2, X3, X4, X5, X6, appendcB_out_ggga(X7, X2, X8, X9)) → U15_GA(X1, X2, X3, X4, X5, X6, inorderA_in_ga(X5, X10))
U14_GA(X1, X2, X3, X4, X5, X6, appendcB_out_ggga(X7, X2, X8, X9)) → INORDERA_IN_GA(X5, X10)
U14_GA(X1, X2, X3, X4, X5, X6, appendcB_out_ggga(X7, X2, X8, X9)) → U16_GA(X1, X2, X3, X4, X5, X6, X9, inordercA_in_ga(X5, X10))
U16_GA(X1, X2, X3, X4, X5, X6, X9, inordercA_out_ga(X5, X10)) → U17_GA(X1, X2, X3, X4, X5, X6, appendC_in_ggga(X9, X4, X10, X6))
U16_GA(X1, X2, X3, X4, X5, X6, X9, inordercA_out_ga(X5, X10)) → APPENDC_IN_GGGA(X9, X4, X10, X6)
APPENDC_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → U7_GGGA(X1, X2, X3, X4, X5, appendC_in_ggga(X2, X3, X4, X5))
APPENDC_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPENDC_IN_GGGA(X2, X3, X4, X5)
inordercA_in_ga(nil, []) → inordercA_out_ga(nil, [])
inordercA_in_ga(tree(X1, X2, X3), X4) → U19_ga(X1, X2, X3, X4, inordercA_in_ga(X1, X5))
U19_ga(X1, X2, X3, X4, inordercA_out_ga(X1, X5)) → U20_ga(X1, X2, X3, X4, X5, inordercA_in_ga(X3, X6))
U20_ga(X1, X2, X3, X4, X5, inordercA_out_ga(X3, X6)) → U21_ga(X1, X2, X3, X4, appendcB_in_ggga(X5, X2, X6, X4))
appendcB_in_ggga([], X1, X2, .(X1, X2)) → appendcB_out_ggga([], X1, X2, .(X1, X2))
appendcB_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U22_ggga(X1, X2, X3, X4, X5, appendcB_in_ggga(X2, X3, X4, X5))
U22_ggga(X1, X2, X3, X4, X5, appendcB_out_ggga(X2, X3, X4, X5)) → appendcB_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U21_ga(X1, X2, X3, X4, appendcB_out_ggga(X5, X2, X6, X4)) → inordercA_out_ga(tree(X1, X2, X3), X4)
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
INORDERD_IN_GA(tree(nil, X1, X2), X3) → U8_GA(X1, X2, X3, inorderA_in_ga(X2, X4))
INORDERD_IN_GA(tree(nil, X1, X2), X3) → INORDERA_IN_GA(X2, X4)
INORDERA_IN_GA(tree(X1, X2, X3), X4) → U1_GA(X1, X2, X3, X4, inorderA_in_ga(X1, X5))
INORDERA_IN_GA(tree(X1, X2, X3), X4) → INORDERA_IN_GA(X1, X5)
INORDERA_IN_GA(tree(X1, X2, X3), X4) → U2_GA(X1, X2, X3, X4, inordercA_in_ga(X1, X5))
U2_GA(X1, X2, X3, X4, inordercA_out_ga(X1, X5)) → U3_GA(X1, X2, X3, X4, inorderA_in_ga(X3, X6))
U2_GA(X1, X2, X3, X4, inordercA_out_ga(X1, X5)) → INORDERA_IN_GA(X3, X6)
U2_GA(X1, X2, X3, X4, inordercA_out_ga(X1, X5)) → U4_GA(X1, X2, X3, X4, X5, inordercA_in_ga(X3, X6))
U4_GA(X1, X2, X3, X4, X5, inordercA_out_ga(X3, X6)) → U5_GA(X1, X2, X3, X4, appendB_in_ggga(X5, X2, X6, X4))
U4_GA(X1, X2, X3, X4, X5, inordercA_out_ga(X3, X6)) → APPENDB_IN_GGGA(X5, X2, X6, X4)
APPENDB_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → U6_GGGA(X1, X2, X3, X4, X5, appendB_in_ggga(X2, X3, X4, X5))
APPENDB_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPENDB_IN_GGGA(X2, X3, X4, X5)
INORDERD_IN_GA(tree(tree(X1, X2, X3), X4, X5), X6) → U9_GA(X1, X2, X3, X4, X5, X6, inorderA_in_ga(X1, X7))
INORDERD_IN_GA(tree(tree(X1, X2, X3), X4, X5), X6) → INORDERA_IN_GA(X1, X7)
INORDERD_IN_GA(tree(tree(X1, X2, X3), X4, X5), X6) → U10_GA(X1, X2, X3, X4, X5, X6, inordercA_in_ga(X1, X7))
U10_GA(X1, X2, X3, X4, X5, X6, inordercA_out_ga(X1, X7)) → U11_GA(X1, X2, X3, X4, X5, X6, inorderA_in_ga(X3, X8))
U10_GA(X1, X2, X3, X4, X5, X6, inordercA_out_ga(X1, X7)) → INORDERA_IN_GA(X3, X8)
U10_GA(X1, X2, X3, X4, X5, X6, inordercA_out_ga(X1, X7)) → U12_GA(X1, X2, X3, X4, X5, X6, X7, inordercA_in_ga(X3, X8))
U12_GA(X1, X2, X3, X4, X5, X6, X7, inordercA_out_ga(X3, X8)) → U13_GA(X1, X2, X3, X4, X5, X6, appendB_in_ggga(X7, X2, X8, X9))
U12_GA(X1, X2, X3, X4, X5, X6, X7, inordercA_out_ga(X3, X8)) → APPENDB_IN_GGGA(X7, X2, X8, X9)
U12_GA(X1, X2, X3, X4, X5, X6, X7, inordercA_out_ga(X3, X8)) → U14_GA(X1, X2, X3, X4, X5, X6, appendcB_in_ggga(X7, X2, X8, X9))
U14_GA(X1, X2, X3, X4, X5, X6, appendcB_out_ggga(X7, X2, X8, X9)) → U15_GA(X1, X2, X3, X4, X5, X6, inorderA_in_ga(X5, X10))
U14_GA(X1, X2, X3, X4, X5, X6, appendcB_out_ggga(X7, X2, X8, X9)) → INORDERA_IN_GA(X5, X10)
U14_GA(X1, X2, X3, X4, X5, X6, appendcB_out_ggga(X7, X2, X8, X9)) → U16_GA(X1, X2, X3, X4, X5, X6, X9, inordercA_in_ga(X5, X10))
U16_GA(X1, X2, X3, X4, X5, X6, X9, inordercA_out_ga(X5, X10)) → U17_GA(X1, X2, X3, X4, X5, X6, appendC_in_ggga(X9, X4, X10, X6))
U16_GA(X1, X2, X3, X4, X5, X6, X9, inordercA_out_ga(X5, X10)) → APPENDC_IN_GGGA(X9, X4, X10, X6)
APPENDC_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → U7_GGGA(X1, X2, X3, X4, X5, appendC_in_ggga(X2, X3, X4, X5))
APPENDC_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPENDC_IN_GGGA(X2, X3, X4, X5)
inordercA_in_ga(nil, []) → inordercA_out_ga(nil, [])
inordercA_in_ga(tree(X1, X2, X3), X4) → U19_ga(X1, X2, X3, X4, inordercA_in_ga(X1, X5))
U19_ga(X1, X2, X3, X4, inordercA_out_ga(X1, X5)) → U20_ga(X1, X2, X3, X4, X5, inordercA_in_ga(X3, X6))
U20_ga(X1, X2, X3, X4, X5, inordercA_out_ga(X3, X6)) → U21_ga(X1, X2, X3, X4, appendcB_in_ggga(X5, X2, X6, X4))
appendcB_in_ggga([], X1, X2, .(X1, X2)) → appendcB_out_ggga([], X1, X2, .(X1, X2))
appendcB_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U22_ggga(X1, X2, X3, X4, X5, appendcB_in_ggga(X2, X3, X4, X5))
U22_ggga(X1, X2, X3, X4, X5, appendcB_out_ggga(X2, X3, X4, X5)) → appendcB_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U21_ga(X1, X2, X3, X4, appendcB_out_ggga(X5, X2, X6, X4)) → inordercA_out_ga(tree(X1, X2, X3), X4)
APPENDC_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPENDC_IN_GGGA(X2, X3, X4, X5)
inordercA_in_ga(nil, []) → inordercA_out_ga(nil, [])
inordercA_in_ga(tree(X1, X2, X3), X4) → U19_ga(X1, X2, X3, X4, inordercA_in_ga(X1, X5))
U19_ga(X1, X2, X3, X4, inordercA_out_ga(X1, X5)) → U20_ga(X1, X2, X3, X4, X5, inordercA_in_ga(X3, X6))
U20_ga(X1, X2, X3, X4, X5, inordercA_out_ga(X3, X6)) → U21_ga(X1, X2, X3, X4, appendcB_in_ggga(X5, X2, X6, X4))
appendcB_in_ggga([], X1, X2, .(X1, X2)) → appendcB_out_ggga([], X1, X2, .(X1, X2))
appendcB_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U22_ggga(X1, X2, X3, X4, X5, appendcB_in_ggga(X2, X3, X4, X5))
U22_ggga(X1, X2, X3, X4, X5, appendcB_out_ggga(X2, X3, X4, X5)) → appendcB_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U21_ga(X1, X2, X3, X4, appendcB_out_ggga(X5, X2, X6, X4)) → inordercA_out_ga(tree(X1, X2, X3), X4)
APPENDC_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPENDC_IN_GGGA(X2, X3, X4, X5)
APPENDC_IN_GGGA(.(X1, X2), X3, X4) → APPENDC_IN_GGGA(X2, X3, X4)
From the DPs we obtained the following set of size-change graphs:
APPENDB_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPENDB_IN_GGGA(X2, X3, X4, X5)
inordercA_in_ga(nil, []) → inordercA_out_ga(nil, [])
inordercA_in_ga(tree(X1, X2, X3), X4) → U19_ga(X1, X2, X3, X4, inordercA_in_ga(X1, X5))
U19_ga(X1, X2, X3, X4, inordercA_out_ga(X1, X5)) → U20_ga(X1, X2, X3, X4, X5, inordercA_in_ga(X3, X6))
U20_ga(X1, X2, X3, X4, X5, inordercA_out_ga(X3, X6)) → U21_ga(X1, X2, X3, X4, appendcB_in_ggga(X5, X2, X6, X4))
appendcB_in_ggga([], X1, X2, .(X1, X2)) → appendcB_out_ggga([], X1, X2, .(X1, X2))
appendcB_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U22_ggga(X1, X2, X3, X4, X5, appendcB_in_ggga(X2, X3, X4, X5))
U22_ggga(X1, X2, X3, X4, X5, appendcB_out_ggga(X2, X3, X4, X5)) → appendcB_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U21_ga(X1, X2, X3, X4, appendcB_out_ggga(X5, X2, X6, X4)) → inordercA_out_ga(tree(X1, X2, X3), X4)
APPENDB_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPENDB_IN_GGGA(X2, X3, X4, X5)
APPENDB_IN_GGGA(.(X1, X2), X3, X4) → APPENDB_IN_GGGA(X2, X3, X4)
From the DPs we obtained the following set of size-change graphs:
INORDERA_IN_GA(tree(X1, X2, X3), X4) → U2_GA(X1, X2, X3, X4, inordercA_in_ga(X1, X5))
U2_GA(X1, X2, X3, X4, inordercA_out_ga(X1, X5)) → INORDERA_IN_GA(X3, X6)
INORDERA_IN_GA(tree(X1, X2, X3), X4) → INORDERA_IN_GA(X1, X5)
inordercA_in_ga(nil, []) → inordercA_out_ga(nil, [])
inordercA_in_ga(tree(X1, X2, X3), X4) → U19_ga(X1, X2, X3, X4, inordercA_in_ga(X1, X5))
U19_ga(X1, X2, X3, X4, inordercA_out_ga(X1, X5)) → U20_ga(X1, X2, X3, X4, X5, inordercA_in_ga(X3, X6))
U20_ga(X1, X2, X3, X4, X5, inordercA_out_ga(X3, X6)) → U21_ga(X1, X2, X3, X4, appendcB_in_ggga(X5, X2, X6, X4))
appendcB_in_ggga([], X1, X2, .(X1, X2)) → appendcB_out_ggga([], X1, X2, .(X1, X2))
appendcB_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U22_ggga(X1, X2, X3, X4, X5, appendcB_in_ggga(X2, X3, X4, X5))
U22_ggga(X1, X2, X3, X4, X5, appendcB_out_ggga(X2, X3, X4, X5)) → appendcB_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U21_ga(X1, X2, X3, X4, appendcB_out_ggga(X5, X2, X6, X4)) → inordercA_out_ga(tree(X1, X2, X3), X4)
INORDERA_IN_GA(tree(X1, X2, X3)) → U2_GA(X1, X2, X3, inordercA_in_ga(X1))
U2_GA(X1, X2, X3, inordercA_out_ga(X1, X5)) → INORDERA_IN_GA(X3)
INORDERA_IN_GA(tree(X1, X2, X3)) → INORDERA_IN_GA(X1)
inordercA_in_ga(nil) → inordercA_out_ga(nil, [])
inordercA_in_ga(tree(X1, X2, X3)) → U19_ga(X1, X2, X3, inordercA_in_ga(X1))
U19_ga(X1, X2, X3, inordercA_out_ga(X1, X5)) → U20_ga(X1, X2, X3, X5, inordercA_in_ga(X3))
U20_ga(X1, X2, X3, X5, inordercA_out_ga(X3, X6)) → U21_ga(X1, X2, X3, appendcB_in_ggga(X5, X2, X6))
appendcB_in_ggga([], X1, X2) → appendcB_out_ggga([], X1, X2, .(X1, X2))
appendcB_in_ggga(.(X1, X2), X3, X4) → U22_ggga(X1, X2, X3, X4, appendcB_in_ggga(X2, X3, X4))
U22_ggga(X1, X2, X3, X4, appendcB_out_ggga(X2, X3, X4, X5)) → appendcB_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U21_ga(X1, X2, X3, appendcB_out_ggga(X5, X2, X6, X4)) → inordercA_out_ga(tree(X1, X2, X3), X4)
inordercA_in_ga(x0)
U19_ga(x0, x1, x2, x3)
U20_ga(x0, x1, x2, x3, x4)
appendcB_in_ggga(x0, x1, x2)
U22_ggga(x0, x1, x2, x3, x4)
U21_ga(x0, x1, x2, x3)
From the DPs we obtained the following set of size-change graphs: